The Timed Concurrent Constraint Language (tccp in short) is a concurrentlogic language based on the simple but powerful concurrent constraint paradigmof Saraswat. In this paradigm, the notion of store-as-value is replaced by thenotion of store-as-constraint, which introduces some differences w.r.t. otherapproaches to concurrency. In this paper, we provide a general framework forthe debugging of tccp programs. To this end, we first present a new compact,bottom-up semantics for the language that is well suited for debugging andverification purposes in the context of reactive systems. We also provide anabstract semantics that allows us to effectively implement debugging algorithmsbased on abstract interpretation. Given a tccp program and a behaviorspecification, our debugging approach automatically detects whether the programsatisfies the specification. This differs from other semiautomatic approachesto debugging and avoids the need to provide symptoms in advance. We show theefficacy of our approach by introducing two illustrative examples. We choose aspecific abstract domain and show how we can detect that a program iserroneous.
展开▼
